$\forall$$M$:MsgA, $k$:Knd, $s$:$M$.state, $v$:$M$.da($k$). $M$.sends($k$,$s$,$v$) $\in$ ($M$.Msg List)